$\forall$$T$:Type, $L$:($T$ List).
\\[0ex](0 $<$ $\parallel$$L$$\parallel$) $\Rightarrow$ no\_repeats($T$;$L$) $\Rightarrow$ ($\forall$$x$:$T$. $x$ before hd($L$) $\in$ $L$ $\Leftarrow\!\Rightarrow$ False)